package alloy.symm;


import java.util.Set;
import java.util.TreeSet;

import alloy.ast.ElemFormula;
import alloy.ast.EmptySetExpr;
import alloy.ast.Leaf;
import alloy.ast.LeafId;
import alloy.ast.NegFormula;

/**
 * Finds unary relations that are constrained to be non-empty.
 * <p>
 * We look for unary relations r for which the fact "some r" is conjoined at the top of the translatable AST formula.
 */
class NonemptySetDetector_V extends TopLevelConjVisitor {
    /**
     * Nonempty sets we have found: {@link LeafId}s of unary relations that --
     * we have determined -- are constrained to be nonemptys in any solution.
     */
    private Set /* of LeafId */ _nonemptySetIds = new TreeSet();
    
    //--------//
    // Methods//
    //--------//
    
    NonemptySetDetector_V() { }

    /** Test whether the given relation is unary and is constrained to contain at least one tuple. */
    boolean isNonemptySet(LeafId leafId_) {
	return _nonemptySetIds.contains(leafId_);
    }

    /**
     * @return the {@link Set} of {@link LeafId}s that are constrained by the
     *         Alloy formula to be DAGs.  Call this after the visitor has
     *         visited the formula.
     */
    Set /* of LeafId */ getNonemptySetIds() { return _nonemptySetIds; }

    /**
     * Look for a formula of the form "not r in none".
     */
    public void visit(NegFormula negFormula_) {
	if (negFormula_.getFormula() instanceof ElemFormula) {
	    ElemFormula ef = (ElemFormula)negFormula_.getFormula();
	    if (_isRelation(ef.getLeft()) && _isUnary(ef.getLeft()) &&
		ef.getRight() instanceof EmptySetExpr)
		_nonemptySetIds.add(((Leaf)ef.getLeft()).getLeafId());
	}
    }
}
